Cleanup of @spcfox's modal logic pull request #1170
Conversation
- Add index for variables in formulas - Add soundness for decidable valuation
- Add priorities
- Add me to contributors
|
Very glad that someone is taking care of this! Do you want a third pair of eyes to look at this before it is merged? |
|
Hello! |
|
Hi @spcfox! I'm glad to hear from you and I hope you are doing well. You have made a heroic effort with your pull request, and indeed I am very happy to take on the task towards merging it. I completely understand that a personal situation might be getting in the way, and you don't need to worry about the pull request if you don't have the energy for it. We will make sure that you will be appropriately attributed for the work that you have done. Take care, and I hope to hear from you again sometime! |
|
Hey! It turns out I might actually have some immediate use of the order theory that is formalized in this PR. Would it be welcome if I extracted that part and wrapped it up in a different PR that could be merged more immediately? @EgbertRijke |
Yes please! Any help is welcome on this PR |
There was a problem hiding this comment.
This file overlaps with foundation.powersets
There was a problem hiding this comment.
At this point, since you are about to make a PR on this, it is probably better to make the changes yourself rather than commenting on them.
There was a problem hiding this comment.
I am, but that doesn't have retroactive power over this PR, which is why I'm commenting on it so that you are aware that the file should be deleted.
There was a problem hiding this comment.
Ah, thanks for clarifying!
There was a problem hiding this comment.
Apologies for the miscommunication!
There was a problem hiding this comment.
No worries! I'm very glad that you're taking a chunk out of this PR! I think that's a very good way to go about it!
Subset of #1146 #1170 --------- Co-authored-by: spcfox Co-authored-by: Egbert Rijke <[email protected]>
@spcfox made an impressive pull request, but unfortunately we haven't heard from him since. This is an attempt to bring his pull request to a mergeable state.